
In this section, we present encodings of %the concept of 
\emph{supervision trees} in our session language 
with located and update processes. 
As supervision trees (as provided by the supervisor module of Erlang~\cite{erlang:sup}) 
define a basic principle for designing and programming fault-tolerant programs, our encodings 
are useful to understand how these our two constructs for runtime adaptation 
(a)~may integrate 
into communicating processes 
%that represent an actual programming mechanism.
and (b)~relate to actual programming mechanisms.

As mentioned in the Introduction, supervision trees organize a program's behavior into two classes: \emph{workers} and \emph{supervisors}. 
Workers are the processes that actually perform computation ---in a com\-mu\-ni\-ca\-tion-centric setting, workers may well correspond to servers which expect and fulfill clients' requests. Supervisors are meant to monitor the behavior of workers by relying on a hierarchical, tree-like structure.
This way, a supervisor may monitor the behavior of a number of children; the supervisor may  itself be supervised by another supervisor at a higher level in the hierarchy. 
As an example, Fig.~\ref{fig:tree} shows a supervisor 
$S_2$ that monitors workers $W_3$ and $W_4$; in turn, $S_2$ is supervised by $S_1$ who is also a supervisor for worker $W_2$.
In Erlang, a supervisor can implement several \emph{restart strategies} which, given a termination signal (e.g. a failure), offer different possibilities for restarting the supervised worker(s). Such strategies are fully detailed in~\cite{erlang:sup}; in what follows, we concentrate on the following two:
%Two of them are the following: %Here we consider only two kinds:
\begin{enumerate}[1.]
 \item \emph{One for one} strategy: if one of the children fails and terminates then only that child is restarted.
 \item \emph{One for all} strategy: if one of the children fails and terminates then all the siblings must be terminated and restarted.
\end{enumerate}



 \begin{figure}[t!]
\begin{center}
  \begin{tikzpicture}
\node [rectangle,draw] (S1){$S_1$}
       child {node [rectangle,draw] (S2) {$S_2$}
                    child {node [circle,draw] (W3) {$W_3$} edge from parent node[above] {$c$~~~}}
                    child {node [circle,draw] (W4) {$W_4$} edge from parent node[above] {~~~$d$}}
                    edge from parent node[above] {$a$~~~}
                    }
       child {node [circle,draw] (W2) {$W_2$}
       edge from parent node[above] {~~~$b$}};
\end{tikzpicture}
 \end{center}
\caption{A supervision tree: supervisors are depicted as rectangles; workers are represented by circles.}\label{fig:tree}
\end{figure}

%\jp{We may mention that supervision trees are interesting for us for they are a real (existing) mechanism that is in line for our intended model of adaptation---something that is external to some behavior and may act autonomously for deciding adaptation routines.}


It is interesting to observe how the hierarchical model for fault-tolerance realized by supervision trees in Erlang is in line with our intended model for runtime adaptation:
in addition to 
the loose analogy between located processes as workers and update processes as supervisors, 
we find useful similarities in terms of hierarchical organization of behavior, 
and in the fact that 
both supervision trees and our update processes 
are in essence  \emph{external} recovery mechanisms for precisely delimited behaviors. 
These intuitions are our starting point for the process representations of supervision trees which we analyze in the rest of this section.
%In the following we provide an encoding of supervision trees in our setting, 
For simplicity, we restrict to representing the hierarchy 
given in Fig.~\ref{fig:tree}, assuming that both $S_1$ and $S_2$ realize the same restarting strategy; the representation, however, can be easily generalized to more complex settings. 
We  represent the tree structure by the nesting of located processes, as follows: %, hence obtaining the process:
\begin{equation}\label{eq:trees}
 \componentbig{l_1}{S_1 \para \componentbbig{l_2}{S_2 \para \compo{w_3}{ }{W_3}\compo{w_4}{ }{W_4} } \para \compo{w_2}{ }{W_2}  }
\end{equation}
In our models, we distinguish between localities for supervisors (denoted $l_i$) and localities for workers (denoted $w_j$).
In the following, we describe two different implementations of supervisors, each realizing a different restarting strategy.
%  depending on the analyzed strategy together with an example of a simple worker.


\subsection{Modeling One for one Supervisors}
As suggested by the above informal description, 
the one for one strategy accounts for a form of \emph{local supervision}: 
whenever a child enters in an error state or fails, the child activity must be terminated and the server restarted. 
This way, for instance, in the scenario of Fig.~\ref{fig:tree}, 
if worker $W_3$ fails then its siblings $W_4$ and $W_2$ should be unaffected by (and unaware of) the restarting process that $S_2$ is expected to initiate.

The one for one strategy can be encoded in a quite natural way within our framework. 
Indeed, 
by assuming that workers correspond to servers which are connected to clients, we may represent 
failures as the reception of an invalid value from the client; the restarting process would then correspond to an update action that simply  recreates the located process containing the server.  
More precisely,  we  assume worker $W_3$ 
is an ``arithmetic server'' which
calculates the division between two natural numbers which are communicated by a client $C$ after establishing a session. 
In this context, failure corresponds to division by zero. 
Then, $W_3$ notifies $S_2$ whether it has found a failure (i.e., the denominator being equal to zero). Subsequently,
$S_2$ should decide what to do next: 
(i) if the denominator sent by the client was zero, then there is indeed a failure and  session between $W_3$ and $C$ must terminate immediately;  (ii) otherwise, if there is not a failure, then $S_2$ should allow $W_3$ to perform the division and communicate the result to $C$. 
Observe how in 
 this ``local'' scenario, supervisor $S_2$ does not need to interact with its supervisor $S_1$.
 
To implement the supervision model described above, every time a worker (such as $W_3$) establishes a session with a client (such as $C$), it also connects to its supervisor. This way,  supervisor and worker have a unique communication mechanism.
%has way to communicate its decisions to its worker.
In our case, this mechanism is realized by a session request from $W_3$ to $S_2$ on name $b$. 
By extending the process in (\ref{eq:trees}) with a client  $C$, we obtain 
the following system:
\begin{equation}\label{eq:tree}
 \componentbig{l_1}{S_1 \para \componentbbig{l_2}{S_2 \para \compo{w_3}{ }{W_3}\compo{w_4}{ }{W_4} } \para \compo{w_2}{ }{W_2}  } \para C
\end{equation}
%$$\compo{l_1}{ }{S_1 \para \compo{l_2}{ }{S_2 \para \compo{w_3}{ }{W_3}\compo{w_4}{ }{W_4} } \para \compo{w_2}{ }{W_2}  } \para C$$
where $S_2$,  $W_3$, and  $C$ are defined as follows (the other processes are left unspecified):
$$
\begin{array}{lcl}
S_2&\triangleq& \repopen{b}{\xb}.\inC{\xb}{v}.\select{\xb}{v}.\ifte{v=\fail}{\close{\xb}.\adaptn{w_3}{\compo{w_3}{}{W_3}}}{\close{\xb}} \\ \\
W_3&\triangleq&\repopen{a}{\xa}.\nopenr{b}{\xb}.\inC{\xa}{u}.\inC{\xa}{v}.\ifte{v=0}{\outC{\xb}{\fail}.P}{\outC{\xb}{\ok}.P} \\
P&\triangleq&\branch{\xb}{\fail: \select{\xa}{\fail}.\close{\xa}.\close{\xb} \parallel \ok: \select{\xa}{\ok}.\outC{\xa}{u \div v}.\close{\xa}.\close{\xb}}\\ \\
C&\triangleq&\nopenr{a}{\xa}.\outC{\xa}{c_1}.\outC{\xa}{c_2}.\branch{\xa}{\fail: \close{\xa} \parallel \ok: \inC{\xa}{v}.\close{\xa}}
\end{array}
$$
%\jp{In $S_2$, is it possible to have $\select{\xb}{v}.\close{\xb}.$ inside the if branches, i.e. 
%$$
%\repopen{b}{\xb}.\inC{\xb}{v}.\ifte{v=\fail}{\select{\xb}{v}.\close{\xb} \para \adaptn{w_3}{\compo{w_3}{0}{W_3}}}{\select{\xb}{v}.\close{\xb}}
%$$
%i think it would be a bit more reasonable (and equivalent)}
%the other actors are left unspecified, but in principle their implementation is similar to the processes given above.
%\jp{please explain how the first action of a worker is to "check in" with his supervisor, via a session request}

Observe how process $S_2$ defines an update action on $w_3$ if $W_3$ communicates to him that the invalid value zero was received.
%Importantly, typing ensures that any update on locality $w_3$ can only happen when all the sessions established by $W_3$ are terminated.
Moreover, using our update construct we can implement more interesting supervisors which go beyond service restarting.
For instance, consider the following process: 
$$S'_2\triangleq \repopen{b}{\xb}.\inC{\xb}{v}.\select{\xb}{v}.\close{\xb}.\ifte{v=\fail}{\adaptn{w_3}{\compo{w_3}{0}{W_3'}}}{\nil}$$
Note how $S'_2$ improves over $S_2$ by placing inside $w_3$ a \emph{different} server behavior, represented by $W'_3$.
Suppose that $W'_3$ represents an upgraded version of $W'_3$ in which the arithmetic server no longer relies on a supervisor in
order to deal with failures/invalid values. This way, whenever $W_3$ communicates a failure to $S'_2$, the resulting update action will
lead to an improved server $W'_3$ that will be able to handle the failure locally, without appealing to an external entity.

%where the final update on locality $w_3$ does not just recreate locality $w_3$ with its worker inside but it could provide a different (upgraded) behavior for it. For instance, this feature can be used to encode the following protocol: if the current version of the worker fails (i.e.  a value 0 has been received from the client) then a new  version of the worker is installed. In the new (upgraded) behavior,  upon reception of a value 0, the worker does not communicate the failure to its supervisor  but  sends a special value to the client and complete in a normal state its session.
%Finally, notice that as locality are transparent they could also be updated from an external entity that wishes to change the behavior of both supervisors and workers.\jp{this last sentence is not very clear}

%\jp{A small disadvantage of the example ``the division server gets 0 from the client'' is that it sounds very similar to the naive example for try/catch/exceptions. we should elaborate on this, saying that our example is just for simplicity and that other kinds of behaviors, including those defined externally to the program's text/behavior (say, the deploy two copies of $W_3$) can be handled in our setting.}

Finally, we briefly discuss the typing of previous processes. Given session types
$$
%\begin{array}{lcl}
 \alpha \triangleq  \tin{\integer}.\tin{\integer}.\oplus\{\fail: \epsilon, \ok: \tout{\integer}.\epsilon \}\quad \text{and} \quad 
  \beta \triangleq  \tin{\str}.\oplus\{\fail: \epsilon, \ok:\epsilon\}
%\end{array}
$$
the processes above are well-typed, given the following environments:
$$
\begin{array}{lcl}
 \Gamma&\supseteq& \{ a:\langle \alpha_{\quau}, \overline{\alpha}_{\qual} \rangle, b:\langle \beta_{\quau}, \overline{\beta}_{\qual}\rangle\}\\
 \Theta&\supseteq& \{l_2:\inter{b}{\beta}{\infty} , w_3:\inter{a}{\alpha}{\infty}, \inter{b}{\overline{\beta}}{\infty}\}
\end{array}
$$
In fact, processes $S_2, W_3$, and $C$ can be typed as follows:
$$
\begin{array}{l}
\judgebis{\env{\Gamma}{\Theta}}{S_2}{\type{\emptyset}{\inter{b}{\beta}{\infty}}}\\
\judgebis{\env{\Gamma}{\Theta}}{W_3}{\type{\emptyset}{\inter{a}{\alpha}{\infty}},\inter{b}{\overline{\beta}}{\infty}}\\
\judgebis{\env{\Gamma}{\Theta}}{C}{\type{\emptyset}{\inter{a}{\overline{\alpha}}{1}}}
\end{array}
$$

Notice that as a consequence of being well-typed, the supervisor has to wait that all sessions have been closed before proceeding with an update of its worker. 


\subsection{Modeling One for all Supervisors}
While the one for one restarting strategy implements a local relation between a worker and his supervisor, 
in the one for all 
%The second strategy is the symmetric with respect to the previous one, in fact here 
strategy  supervisors need to globally control their children. Hence, whenever one of the children enters in an error state, the child and its siblings have to be terminated and restarted. For instance, in the scenario of Fig.~\ref{fig:tree}, 
if $W_2$ fails then both $W_2$ and all the workers contained in the subtree rooted in $S_2$ need to be terminated and restarted. 
This event should be communicated by $S_1$ to $S_2$, which should handle the termination of its children.
% \jp{I would say: ``It is plausible to think that in such a case $S_1$ would send a signal to $S_2$ bla bla''}. 
On the other hand, if $W_3$ fails then its supervisor $S_2$ only has to stop $W_4$, and nothing needs to be communicated to $S_1$.

The required global control that supervisors should exercise over children in the one for all strategy turns out to be
slightly unnatural to express in our framework of binary communication.
%It is clear, then, that supervisors in a one-for-all strategy need to have a global control on children, and this is somehow less natural to express in our formalism. \jp{I'd add: 
Nevertheless, it is possible to devise a protocol that achieves the desired synchronization sequences.
An alternative to represent global synchronization among services and supervisors is described by the following informal protocol,
in which communication between workers and clients (and between supervisors and workers) is managed via session establishment: 
\begin{enumerate}[1.]
 \item %Each service located in a worker performs one step, i.e. 
 Each worker receives a data value $v$ from a client. The value is checked for validity (via a boolean expression $e(v)$). The result of this check is sent to the worker's supervisor.
 \item Each supervisor waits to receive the result of the validity check from  all its children.
 \item Each supervisor (apart from the root node $S_1$) sends a $\true$ value to its own supervisor. This is to have a uniform communication pattern, and is related to the fact that supervisors themselves cannot fail.
 \item Starting from the root of the tree, a communication cascade takes place: each supervisor communicates to its children if they can continue with their own service or if they have to terminate. Intuitively,  a single worker can continue if and only if (i) none of its siblings have failed and (ii) the supervisor has not received from its own supervisor a failure signal.
 \item If a worker (server) receives a failure signal, then it stops the communications with its clients; otherwise, it can continue with its intended behavior.
 \item Finally, when a worker/server stops it is recreated by its supervisor.  
In the case of a forced termination this corresponds to the actual restarting strategy; in the case of natural termination, this enables server persistency.
In the process $Q$ below, this is realized via an update. Notice that $S_1$ will need to recreate only $W_2$, while $S_2$ will be responsible for the restart of its own children $W_3$ and $W_4$. 
\end{enumerate}

%\jp{similar to a previous comment, this is a bit too focused on failures related with specific data values, so it conveys the idea of exceptions. we should say that the values communicated may not necessarily be data from the client, but system parameters, flags and other infrastructure-related stuff, for instance.}

%\jp{I assume that from now on the text needs to be expanded... to explain the model, for instance}.
Notice that Fig.~\ref{fig:tree} already shows in the edges the names of the services established between each pair. As before,
 we consider a process structure as in (\ref{eq:tree}). %, extended with an instance of a client $C$. %: \jp{the following is redundant, right? it's just like the one before..}
%$$\compo{l_1}{0}{S_1 \para \compo{l_2}{0}{S_2 \para \compo{w_3}{0}{W_3}\compo{w_4}{0}{W_4} } \para \compo{w_2}{0}{W_2}  } \para C$$
Here we just give the encoding of worker $W_3$---the other workers  have analogous representations. 
Moreover, we suppose that $W_3$ can establish a session $i$ with client $C$. 
Notice that each worker can establish a session with just one client at the time.
We have:
$$
\begin{array}{ll}
W_3::=&\nopena{i}{\xj}.\nopenr{c}{\xc}.\inC{\xj}{v}.\ifte{e(v)}{\outC{\xc}{\ok}.P}{\outC{\xc}{\fail}.P} \\
P::=&\inC{\xc}{y}.\select{\xc}{y}.\branch{\xc}{\fail: \select{\xj}{\fail}.\close{\xj}.\close{\xc} \parallel \ok: \select{\xj}{\ok}.\proto_W.\close{\xj}.\close{\xc}}\\ 
C::=& \nopenr{i}{\xj}.\outC{\xj}{c}.\branch{\xj}{\fail: \close{\xj} \parallel \ok: \proto_C.\close{\xj}} \\ \\
% \end{array}
% $$
% 
% $$
% \begin{array}{ll}
S_2::= &\repopen{c}{\xc}.\nopena{d}{\xd}.\nopenr{a}{\xa}.\inC{\xc}{u}.\inC{\xd}{v}.\outC{\xa}{\true}.\inC{\xa}{z}.\select{\xa}{z}.\\
& \ifte{u \wedge v \wedge (z= \ok)}
       {\outC{\xc}{\ok}.\outC{\xd}{\ok}.R}
       {\outC{\xc}{\fail}.\outC{\xd}{\fail}.R}\\
R::= & \branch{\xc}{\fail: \select{\xc}{\fail}.\branch{\xd}{\fail: \select{\xd}{\fail}.\close{\xc}.\close{\xd}.\close{\xa}.Q } \parallel \\
& \qquad \     \ok:\select{\xc}{\ok}.\branch{\xd}{\ok: \select{\xd}{\ok}.\proto_{S2}.\close{\xc}.\close{\xd}.\close{\xa}.Q }}\\
Q::=& \adaptn{w_3}{\compo{w_3}{ }{W_3}} \para \adaptn{w_4}{\compo{w_4}{ }{W_4}} \\ \\
% \end{array}
% $$
% 
% $$
% \begin{array}{ll}
S_1::=&\repopen{a}{\xa}.\nopena{b}{\xb}.\inC{\xa}{u}.\inC{\xb}{v}.\ifte{u \wedge v }
       {\outC{\xa}{\ok}.\outC{\xb}{\ok}.T}
       {\outC{\xa}{\fail}.\outC{\xb}{\fail}.T}\\
T::= & \branch{\xa}{\fail: \select{\xa}{\fail}.\branch{\xb}{\fail: \select{\xb}{\fail}.\close{\xa}.\close{\xb}.\adaptn{w_2}{\compo{w_2}{ }{W_2}} } \parallel \\
& \qquad \     \ok:\select{\xa}{\ok}.\branch{\xb}{\ok: \select{\xb}{\ok}.\proto_{S1}.\close{\xa}.\close{\xb}.\adaptn{w_2}{\compo{w_2}{ }{W_2}} }}
\end{array}
$$

Above, $\proto_W$, $\proto_C$, and $\proto_{Si}$ denote the rest of the behavior of workers, clients and supervisors; as such, we assume that and $\proto_W$ and $\proto_C$ are the dual of each other.
Observe how  as soon as worker $W_3$ has established a session on $i$ with the client, it contacts its own supervisor through $c$ and implements step (1) of the protocol above, then it waits for the decision of the supervisor. Similarly for its supervisor $S_2$: after it has established a session for each worker ($W_3$ and $W_4$) through services $c$ and $d$ respectively, it contacts $S_1$ via $a$ and implements steps (2) and (3) of the protocol. Finally, the root supervisor $S_1$ will take a decision and communicate to its workers whether they have to terminate or continue. Then it will pass the information to (child) supervisor $S_2$, that in turn will rule the behavior of its children (cf. steps (4) and (5)). As a last step (point (6)) each supervisor will take care of recreating of its own children.

The system above can be shown to be well-typed, analogously as we did for the process representation for the one for one strategy.
%Analogously as before the system described here is well-typed, 
Here again, typing ensures that no session is disrupted while communication with clients is still active.

%\todo{Maybe now we need to play a bit with the examples...}\jp{and extend the explanation?}
